Nuprl Lemma : csupdate?_wf
11,40
postcript
pdf
Cmd
:Type,
x
:chain_sys(
Cmd
). csupdate?(
x
)
latex
Definitions
s
=
t
,
t
T
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
Id
,
type
List
,
tt
,
ff
,
,
x
.
A
(
x
)
,
x
,
y
.
t
(
x
;
y
)
,
x
.
t
(
x
)
,
chain_sys_ind(
x
;
cmd
.
input
(
cmd
);
from
,
cmds
.
update
(
from
;
cmds
))
,
Type
,
chain_sys(
Cmd
)
,
csupdate?(
x
)
,
a
:
A
fp
B
(
a
)
,
strong-subtype(
A
;
B
)
,
P
Q
Lemmas
member
wf
,
chain
sys
wf
,
chain
sys
ind
wf
,
bool
wf
,
bfalse
wf
,
btrue
wf
,
Id
wf
origin
Cmd:Type, x:chain_sys(Cmd). csupdate?(x) 
Cmd:Type, x:chain_sys(Cmd). csupdate?(x) T
B(x)x:A. B(x)
x.A(x)
x,y. t(x;y)x. t(x) B(a)
Q